\begin{tabbing}
$\forall$$D$:Dsys.
\\[0ex]Feasible($D$)
\\[0ex]$\Rightarrow$ \=(\=$\forall$${\it dec}$:($i$,$a$:Id$\rightarrow\mathbb{N}\rightarrow$M($i$).state$\rightarrow$(?if $a$ $\in$ dom(M($i$).prob) then Outcome else Void fi )),\+\+
\\[0ex]$i$:Id.
\-\\[0ex]d{-}machine($i$;M($i$);${\it dec}$($i$))
\\[0ex]$\in$ w{-}automaton($\lambda$$x$.M($i$).ds($x$);$\lambda$$a$.M($i$).da(locl($a$));$\lambda$$l$,${\it tg}$. M(source($l$)).dout($l$,${\it tg}$)))
\-
\end{tabbing}